package interfaces;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;



@Init ({"getDescripcion()!=null"})
@Inv ({""})

public interface IListaDeProductosComprados {
	
	@Query
	public String getDescripcion();
	
	@Query 
	public int getIdLista();
	
	@Pre ({"nuevaDescripcion!=null #NullPointerException"})
	@Pos ({"getDescripcion().equals(nuevaDescripcion) && getIdLista()==getIdLista()@pre"})
	public void setDescripcion(String nuevaDescripcion);
	
	@Pre ({"l>=0 && l<= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos({"getIdLista()== l && getDescripcion().equals(getDescripcion()@pre)"})
	public void setIdLista(int l);
}
